CHOICE-STRATEGY-IS: 
ANCESTRY;

EDIT-STRATEGY-IS: 
DEPTH[1]∨LENGTH[1];

ELAPSED-TIME =583

NIL 1 2
1 ¬P;AXIOM
2 P;AXIOM